#include <vector>
#include <cassert>
#include <algorithm>
#include <iostream>
#include <fstream>
#include <ctime>
#include <cstring>

using std::cout;
using std::endl;
using std::vector;
using std::ofstream;

typedef unsigned short minterm_t; // UP To 16 variable 
typedef unsigned       cube_t;    // a cube (implicant)
const char * name[16] = {"d","c","b","a"};
static const unsigned Logic0 = 0;
static const unsigned Logic1 = 1;
static const unsigned LogicX = 2;

static void print_cube( cube_t a , int s )
{
   for( int i = 0 ; i < s ; ++i , a = a >> 2 )
   {
      assert( (a&3) != 3 );
      if( (a&3) == LogicX ) continue;
      if( (a&3) == 0 ) cout<<"-";
      cout << name[i] <<" " ;
   }
   cout<<endl;
}
unsigned count_bits( unsigned int x)
{
   x = (x & 0x55555555) + ((x & 0xaaaaaaaa) >> 1);
   x = (x & 0x33333333) + ((x & 0xcccccccc) >> 2);
   x = (x & 0x0f0f0f0f) + ((x & 0xf0f0f0f0) >> 4);
   x = (x & 0x00ff00ff) + ((x & 0xff00ff00) >> 8);
   x = (x & 0x0000ffff) + ((x & 0xffff0000) >> 16);
   return x;
}
static unsigned distence( cube_t a , cube_t b )
{
   return count_bits( a ^ b );
}
static cube_t merge( cube_t a , cube_t b )
{
   assert( distence( a , b ) == 1 );
   cube_t mask = a ^ b; 
   return (a | (mask<<1)) & (~mask) ;
}
static unsigned minterm2cube( unsigned short x)
{ 
   unsigned cube = 0;
   unsigned mask = 1;
   for( ; x ; x = x>>1 , mask = mask << 2 )
      if( x & 1 ) cube |= mask; 

   return cube;
}
static bool bitlt( unsigned a , unsigned b )
{
   return count_bits(a) < count_bits( b);
}

//
//  Given the cube --> producing the prime implicant 
//  (Recursive)
//  1. try merge the neighbor 
//  2. recursive call 
//  3. update and return 
//
static void merge_cube( vector<cube_t> & cubes , vector<unsigned> & flags )
{
//   for( int i = 0 ; i < cubes.size() ; ++i )
//      print_cube( cubes[i] , 4 );cout<<endl;

   bool mark[cubes.size()];
   memset( mark , 0 , sizeof( bool ) * cubes.size() );
   
   vector<cube_t> ncubes;
   vector<unsigned> nflags; nflags.push_back( 0 );
   unsigned n=0;

   for( unsigned int i = 0 ; i < flags.size()-2; ++i )
   {
      n = ncubes.size();

      for( unsigned int j = flags[i] ; j < flags[i+1] ; ++j )
      {
         for( unsigned int k = flags[i+1] ; k < flags[i+2] ; ++k )
         {
            if( distence( cubes[j] , cubes[k] ) == 1 )
            {
               ncubes.push_back( merge( cubes[j] , cubes[k] ) );
               mark[j] = mark[k] = true;
            }
         }
      }

      if( n != ncubes.size() )
      {
         sort( ncubes.begin() + n , ncubes.end() );
         for( unsigned int j = n+1 ; j < ncubes.size() ; ++ j )
            if( ncubes[n] != ncubes[j] )
               ncubes[++n] = ncubes[j];
         n+=1;
         ncubes.resize( n );
      }
      nflags.push_back(n);
   }
   if( n != 0)
      merge_cube( ncubes , nflags );

   int j=0;
   for( unsigned int i = 0 ; i < cubes.size() ; ++i )
      if( mark[i] == false ) cubes[j++] = cubes[i];
   cubes.resize( j );
   
   for( unsigned int i = 0 ; i < ncubes.size() ; ++ i ) 
      cubes.push_back( ncubes[i] );
}

//single function generate prime implicant 
static void generate_all_primes( vector<minterm_t> & onset , vector<cube_t> & primes )
{
   //sort the onset  
   vector<unsigned> flags;flags.push_back(0);

   std::sort( onset.begin() , onset.end() , bitlt );
   unsigned cnt = count_bits( onset[0] );

   for( unsigned int i = 0 ; i < onset.size() ; ++i )
      primes.push_back( minterm2cube( onset[i] ) );

   for( unsigned int i = 1 ; i < onset.size() ; ++i )
   {
      if( count_bits( onset[i] ) != cnt )
      {
         cnt = count_bits( onset[i] );
         flags.push_back( i );
      }
   }
   flags.push_back( onset.size() );
   merge_cube( primes , flags ); 
}
unsigned DONT_CARE = 0xAAAAAAAA;
unsigned CARE      = 0x55555555;
static bool cover( cube_t p , minterm_t m )
{
   cube_t care = (~((p&DONT_CARE) >> 1))& CARE;
   return ((minterm2cube(m) ^ p ) & care) == 0 ;
}
static void unate_cover( vector<minterm_t> & onset , vector<cube_t> & primes )
{
   vector<unsigned> covered_by_primes[ onset.size() ];
   vector<unsigned> cover_minterm[ primes.size() ];

   for( unsigned int j = 0 ; j < onset.size() ; ++j )
   {
      for( unsigned int i = 0 ; i < primes.size() ; ++ i)
      {
         if( cover( primes[i], onset[j] ) )
         {
//            cout << '*';
            cover_minterm[i].push_back( j );
            covered_by_primes[j].push_back(i);
         }else
         {
//            cout << ' ';
         }
      }
//      cout <<"\n";
   }

   ofstream out( "tmp.opb" );

   out << "min: ";
   for( unsigned int i = 0 ; i < primes.size() ; ++ i )
      out << "+" << cover_minterm[i].size() << "*x"<< i <<" ";
   out<<";\n";
   
   for( unsigned int i = 0 ; i < onset.size() ; ++i )
   {
      for( unsigned int j = 0 ; j < covered_by_primes[i].size() ; ++ j )
         out << "+1*x" << covered_by_primes[i][j] << " ";
      out <<">= 1;\n";
   }
   out.close();

   FILE * f = popen( "minisat+ tmp.opb -v0" , "r" );
   assert( f );
   unsigned idx = 0 , num = 0;
   char buf[32];
   while( ! feof( f ) && num != primes.size())
   {
      fscanf( f , "%s" , buf );
      if( buf[0] == 'x')
      {
         assert( atoi( buf+1) == num );
         primes[ idx ++ ] = primes[ num ++ ];
      }
      else if ( buf[0] == '-' && buf[1] =='x' )
      {
         assert( atoi( buf+2) == num );
         num ++ ;
      }
   }
   primes.resize( idx );

   fclose( f );
}
void quine_mccluskey( vector<minterm_t> & onset , vector<cube_t> & primes )
{
   generate_all_primes( onset , primes );
   unate_cover( onset , primes );
}
void fun2minterm( vector<minterm_t> & onset , unsigned short fun )
{
   for( unsigned i = 0 , j = 1 ; i  < 16 ; ++ i , j = j << 1 )
      if( fun & j )
         onset.push_back(i);
}

